A:Type, B:(A
Type), Q:(x:AB(x)Type).
(
x:A. 
y:B(x). Q(x,y)) 
(f:x:AB(x). (x:A. Q(x,f(x))))
ProofTree
| 12,41 |
A:Type, B:(AType), Q:(x:AB(x)Type).
x:A. y:B(x). Q(x,y)) (f:x:AB(x). (x:A. Q(x,f(x))))
| Definitions |  Tx:A. B(x) Qx:A. B(x)  x. t(x) |
| Lemmas |